Mechanization of pomset languages in the Coq proof assistant for the specification of weak memory models
Annotation
Memory models define semantics of concurrent programs operating on shared memory. Theory of these models is an active research topic. As new models emerge, the problem of providing a rigorous formal specification of these models becomes relevant. In this paper we consider a problem of formalizing memory models in the interactive theorem proving systems. We use semantic domain of pomset languages to formalize memory models. We propose an encoding of pomset languages using quotient types and discuss advantages and shortcomings of this approach. We present a library developed in the Coq proof assistant that implements the proposed approach. As a part of this library, we establish a connection between pomset languages and operational semantics defined by labeled transition systems. With the help of this theory, it becomes possible to define in Coq memory models parameterized by the operational semantics of an abstract datatype, and thus to decouple the definition of a memory model from the definition of the datatype. The proposed library can be used to develop formal machine-checked specifications of a wide class of memory models. In order to demonstrate its applicability, we present specifications of several basic memory models: sequential, causal, and pipelined consistency.
Keywords
Постоянный URL
Articles in current issue
- Methods for audiovisual recognition of people in masks
- Influence of the ratio of the intensities of the reference and object waves on the intensity distribution in the holographic field
- High-precision fiber-optic temperature sensor based on Fabry-Perot interferometer with reflective thin-film multilayer structures
- Optical system design method for the concentration of radiation from a high-power LED
- Detection of potholes on road surfaces using photogrammetry and remote sensing methods
- Adaptive control of nonlinear plant with unmatched parametric uncertainties and input saturation
- Application of failure detection methods to detect information attacks on the control system
- DC motor fault detection and isolation scheme with the use of directional residual set
- Synthesis and implementation of λ-approach of slide control in heat-consumption system
- Photocatalytic properties of Ag-AgBr nanostructures in ion-exchanged layers of bromide sodium-zinc-aluminosilicate glass matrix
- Cloud-based intelligent monitoring system to implement mask violation detection and alert simulation
- Efficient incremental hash chain with probabilistic filter-based method to updateblockchain light nodes
- Method for generating masks on face images and systems for their recognition
- Improving sign language processing via few-shot machine learning
- Quantum-probabilistic SVD: complex-valued factorization of matrix data
- Modelling of basic Indonesian Sign Language translator based on Raspberry Pi technology
- A method of multimodal machine sign language translation for natural human-computer interaction
- Web app for quick evaluation of subjective answers using natural language processing
- Substantiation of construction and evaluation ways of the application efficiency for spatially distributed system of information sensors to provide environment monitoring
- Monitoring of infiltration processes in hydraulic structures using distributed acoustic sensing technology
- Slotted waveguide antenna design for maritime radar system